package com.szeldon.pj.jps.exp;

import java.util.List;

import com.szeldon.pj.jps.data.store.SBAStore;
import com.szeldon.pj.jps.datastore.BooleanObject;
import com.szeldon.pj.jps.datastore.SBAObject;
import com.szeldon.pj.jps.datastore.SimpleObject;
import com.szeldon.pj.jps.envs.ENVS;
import com.szeldon.pj.jps.envs.ENVSBinder;
import com.szeldon.pj.jps.envs.ENVSStackFrame;
import com.szeldon.pj.jps.qres.AbstractQueryResult;
import com.szeldon.pj.jps.qres.BagResult;
import com.szeldon.pj.jps.qres.BooleanResult;
import com.szeldon.pj.jps.qres.QResStack;
import com.szeldon.pj.jps.qres.ReferenceResult;
import com.szeldon.pj.jps.visitor.ASTVisitor;

public class ForallBinaryExpression extends BinaryExpression {

	/**
	 * 
	 * @param leftExpression
	 * @param rightExpression
	 */
	public ForallBinaryExpression(Expression leftExpression, Expression rightExpression) {
		super(leftExpression, rightExpression);
	}

	public void accept(ASTVisitor astVisitor, ENVS envs, QResStack qResStack, SBAStore store) {

		astVisitor.accept(leftExpression);

		BagResult expressionResult = new BagResult();
		AbstractQueryResult qResStackPoppedResult = qResStack.pop();

		if (!(qResStackPoppedResult instanceof BagResult)) {
			throw new IllegalStateException("Forall expression expects result of left subexpression to be of "
					+ "BagResult type. Currently it is " + qResStackPoppedResult.getClass().getName() + ".");
		}

		BagResult leftResultsBag = (BagResult) qResStackPoppedResult;
		if (leftResultsBag.getElementsSize() == 0) {
			expressionResult.addResult(new BooleanResult(true));
		} else {

			boolean toReturnInBag = true;
			for (AbstractQueryResult currentLeftResult : leftResultsBag.getElements()) {
				List<ENVSBinder> bindersList = envs.nested(currentLeftResult, store);
				envs.push(new ENVSStackFrame(bindersList));

				astVisitor.accept(rightExpression);
				envs.pop();

				AbstractQueryResult rightResult = qResStack.pop();
				if (!(rightResult instanceof BooleanResult) && !(rightResult instanceof BagResult)) {
					throw new IllegalStateException("Forall expression needs right expression to be a BooleanResult "
							+ "or BagResult with one NameExpression that references to BooleanObject. "
							+ "Currently it's of " + rightResult.getClass().getName() + " type.");
				}

				if (rightResult instanceof BooleanResult) {
					boolean currentRightSubresultValue = ((BooleanResult) rightResult).getBool();
					if (!currentRightSubresultValue) {
						toReturnInBag = false;
					}
				} else {

					AbstractQueryResult firstRightSubresult = ((BagResult) rightResult).getElements().iterator().next();
					if (firstRightSubresult instanceof ReferenceResult) {

						SBAObject retrievedObject = store.retrieve(((ReferenceResult) firstRightSubresult)
								.getReferencedObjectId());
						if (retrievedObject instanceof BooleanObject) {
							boolean currentRightSubresultValue = ((BooleanObject) retrievedObject).getValue();
							if (!currentRightSubresultValue) {
								toReturnInBag = false;
							}
						} else {
							throw new IllegalStateException(
									"Forall expression needs right expression to be a BooleanResult "
											+ "or BagResult with one ReferenceResult for BooleanObject. "
											+ "Currently it's of " + rightResult.getClass().getName()
											+ " type and retrieved object is of "
											+ retrievedObject.getClass().getName() + " type.");
						}
					} else {
						throw new IllegalStateException(
								"Forall expression needs right expression to be a BooleanResult "
										+ "or BagResult with one ReferenceResult for BooleanObject. "
										+ "Currently it's of " + rightResult.getClass().getName()
										+ " type and first result in it is of "
										+ firstRightSubresult.getClass().getName() + " type.");
					}
				}
			}

			expressionResult.addResult(new BooleanResult(toReturnInBag));
		}

		qResStack.push(expressionResult);

	}

	@Override
	public int compareTo(SimpleObject object) throws IllegalStateException {
		// TODO Auto-generated method stub
		return 0;
	}

	@Override
	public String getValueAsString() {
		return "forall";
	}

}
